Closes #815

@Paul-Lez — applied the mechanical nits in 5991646, on top of an upstream/main merge: @[category undergraduate] → @[category textbook] (and copyright 2026 where applicable). The substantive content comments on this PR (open characterization vs. existence/universal phrasing, etc.) are tracked separately and will be addressed in follow-up commits per PR.

Thanks for the review @PaulLez. Pushed 066b374 on add-problem-596: the headline now asserts characterization (pointwise iff with a conjectural predicate behind answer(sorry)), and the existence-of-one-pair statement is demoted to a variant erdos_596.variants.exists_exceptional.

Thanks @mo271 for the review. Pushed 4adc06f addressing all four points:

1. Edge-colouring disjointness. IsNEdgeColouring and IsCountableEdgeColouring now require pairwise disjointness of colour classes (∀ i j, i ≠ j → Disjoint (c i) (c j)) in addition to the union being H. This fixes both the Ramsey direction (HasFiniteRamseyProperty was too strong) and the escape direction (HasCountableRamseyEscape was too weak).

2. Use Mathlib IsContained / Free. Removed the local ContainsCopy and IsFree definitions; the file now uses SimpleGraph.IsContained (notation ⊑) and SimpleGraph.Free from Mathlib.Combinatorics.SimpleGraph.Copy directly.

3. Deduped problem statement. Trimmed the module docstring to title + *References:* block. The full statement appears only in the erdos_596 theorem docstring now (the duplicate ## Overview section has been removed).

4. Universe consistency. Changed original_conjecture_is_false from Type* to Type to match the rest of the file.

Local lake build FormalConjectures.ErdosProblems.«596» succeeds.

Thanks. Already much better (and likely mathematically now not wrong anymore). More review comments:

1. ForMathlib: Unify edge-colouring definitions

IsNEdgeColouring and IsCountableEdgeColouring are nearly identical — they differ only in the index type (Fin n vs ℕ). Please unify them into a single definition parameterized by the index type and place it in FormalConjecturesForMathlib/Combinatorics/SimpleGraph/EdgeColouring.lean:

def IsEdgeColouring {V ι : Type*} (H : SimpleGraph V) (c : ι → SimpleGraph V) : Prop :=
  H = ⨆ i, c i ∧ ∀ i j, i ≠ j → Disjoint (c i) (c j)

The two current definitions become
IsEdgeColouring H (c : Fin n → _) and IsEdgeColouring H (c : ℕ → _) respectively.

2. ForMathlib: Ramsey definitions

HasFiniteRamseyProperty, HasCountableRamseyEscape, and IsErdosHajnalExceptional are general graph-theoretic concepts that would be reusable by Problem 595 and other Ramsey-type problems. Please move them to FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Ramsey.lean (or similar).

3. Don't repeat status in docstrings

Please remove the Status: OPEN / Status: SOLVED / Status: SOLVED (FALSE) lines from the docstrings (e.g., lines 96, 111, 124, 137, 150, 162, 176, 188). The status is already encoded in the @[category research open] / @[category research solved] attribute — repeating it in prose is redundant and creates a maintenance burden if the status changes.

4. Docstring duplication

The $(C_4, C_6)$ example is described in 4 separate docstrings (erdos_596, C4_free_countable_escape, C4_C6_finite_ramsey, C4_C6_is_exceptional). The individual variant docstrings should briefly state what they prove without re-explaining the full context already given in the main docstring.

5. No tests

Consider adding @[category test] sanity checks — e.g., that cycleGraph 4 ≠ ⊥, or basic properties of IsEdgeColouring.